package br.edu.ufcg.symbolrt.examples;

import br.edu.ufcg.symbolrt.base.Action;
import br.edu.ufcg.symbolrt.base.ClockGuard;
import br.edu.ufcg.symbolrt.base.Location;
import br.edu.ufcg.symbolrt.base.SimpleClockGuard;
import br.edu.ufcg.symbolrt.base.TIOSTS;
import br.edu.ufcg.symbolrt.base.TypedData;
import br.edu.ufcg.symbolrt.util.Constants;

public class TargetDesignation {
	
	 public static TIOSTS createSPEC(){
		 TIOSTS tiosts = new TIOSTS("Target Designation");
		 
		 // Clocks and their guards
		 
		 tiosts.addClock("clock1");	
         SimpleClockGuard guard1 = new SimpleClockGuard(2, "clock1", Constants.GUARD_EQUAL, "200");
 		 ClockGuard clockGuard1 = new ClockGuard();
 		 clockGuard1.addSimpleClockGuard(guard1); 		 		 
		 
         // Variables
         TypedData targetTD = new TypedData("targetTD", Constants.TYPE_INTEGER);
         tiosts.addVariable(targetTD);
         TypedData modeTD = new TypedData("modeTD", Constants.TYPE_INTEGER);
         tiosts.addVariable(modeTD);
         TypedData azimuthTD = new TypedData("azimuthTD", Constants.TYPE_INTEGER);
         tiosts.addVariable(azimuthTD);
         TypedData elevationTD = new TypedData("elevationTD", Constants.TYPE_INTEGER);
         tiosts.addVariable(elevationTD);
         TypedData latitudeTD = new TypedData("latitudeTD", Constants.TYPE_INTEGER);
         tiosts.addVariable(latitudeTD); 
         TypedData longitudeTD = new TypedData("longitudeTD", Constants.TYPE_INTEGER);
         tiosts.addVariable(longitudeTD);
         TypedData altitudeTD = new TypedData("altitudeTD", Constants.TYPE_INTEGER);
         tiosts.addVariable(altitudeTD); 


         
         // Parameters
         TypedData id = new TypedData("id", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(id);
         TypedData op = new TypedData("op", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(op);
         TypedData a = new TypedData("a", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(a);
         TypedData e = new TypedData("e", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(e);
         TypedData la = new TypedData("la", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(la);
         TypedData lo = new TypedData("lo", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(lo);
         TypedData al = new TypedData("al", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(al);
         TypedData r = new TypedData("r", Constants.TYPE_INTEGER);
         tiosts.addActionParameter(r);

         
         // Input, output, and internal actions
         Action init = new Action("init1", Constants.ACTION_INTERNAL);
         tiosts.addAction(init);
         
         Action selectTD = new Action("selectTD", Constants.ACTION_INPUT);
         selectTD.addParameter(id.getName());
         selectTD.addParameter(op.getName());
         tiosts.addAction(selectTD);
         
         Action undesignate = new Action("undesignate", Constants.ACTION_OUTPUT);
         undesignate.addParameter(id.getName());
         tiosts.addAction(undesignate);
         
         Action changeModeHUD = new Action("changeModeHUD", Constants.ACTION_OUTPUT);
         tiosts.addAction(changeModeHUD);
         
         Action reticlePositionHUDIn = new Action("reticlePositionHUD", Constants.ACTION_INPUT);
         reticlePositionHUDIn.addParameter(a.getName());
         reticlePositionHUDIn.addParameter(e.getName());
         tiosts.addAction(reticlePositionHUDIn);
         
         Action designate = new Action("designate", Constants.ACTION_OUTPUT);
         designate.addParameter(id.getName());
         tiosts.addAction(designate);
         
         Action reticlePositionHUDOut = new Action("reticlePositionHUD", Constants.ACTION_OUTPUT);
         reticlePositionHUDOut.addParameter(a.getName());
         reticlePositionHUDOut.addParameter(e.getName());
         tiosts.addAction(reticlePositionHUDOut);
         
         Action changeModeRadar = new Action("changeModeRadar", Constants.ACTION_OUTPUT);
         tiosts.addAction(changeModeRadar);
         
         Action aircraftPosition = new Action("aircraftPosition", Constants.ACTION_INPUT);
         aircraftPosition.addParameter(r.getName());
         aircraftPosition.addParameter(a.getName());
         aircraftPosition.addParameter(e.getName());
         tiosts.addAction(aircraftPosition);
         
         Action targetPosition = new Action("targetPosition", Constants.ACTION_INPUT);
         targetPosition.addParameter(r.getName());
         targetPosition.addParameter(a.getName());
         targetPosition.addParameter(e.getName());
         tiosts.addAction(targetPosition);
         
         Action track = new Action("track", Constants.ACTION_OUTPUT);
         track.addParameter(id.getName());
         tiosts.addAction(track);
         
         
         Action finishTargetDesignation = new Action("finishTargetDesignation", Constants.ACTION_OUTPUT);
         finishTargetDesignation.addParameter(op.getName());
         tiosts.addAction(finishTargetDesignation);
                  
         // Locations
         Location start = new Location("Start1");
         tiosts.addLocation(start);
         Location S9 = new Location("S9");
         tiosts.addLocation(S9);
         Location S10 = new Location("S10");
         tiosts.addLocation(S10);     
         Location S11 = new Location("S11");
         tiosts.addLocation(S11);
         Location S12 = new Location("S12");
         tiosts.addLocation(S12); 
         Location S13 = new Location("S13");
         tiosts.addLocation(S13); 
         Location S14 = new Location("S14");
         tiosts.addLocation(S14); 
         Location S15 = new Location("S15");
         tiosts.addLocation(S15); 
         Location S16 = new Location("S16");
         tiosts.addLocation(S16); 
         Location S17 = new Location("S17");
         tiosts.addLocation(S17); 
         Location S18 = new Location("S18");
         tiosts.addLocation(S18); 
         Location S19 = new Location("S19");
         tiosts.addLocation(S19); 
         
         // Initial Condition
         tiosts.setInitialCondition(Constants.GUARD_TRUE);
         
         // Initial Location
         tiosts.setInitialLocation(start);
         
         // Transitions
         tiosts.createTransition("Start1", Constants.GUARD_TRUE, Constants.GUARD_TRUE, init, null, null, "S9");
         tiosts.createTransition("S9", Constants.GUARD_TRUE, Constants.GUARD_TRUE, selectTD, "modeTD := op | targetTD := id", null, "S10");
         //undesignation target assumes 1
         tiosts.createTransition("S10", "modeTD = 1 AND targetTD = id", Constants.GUARD_TRUE, undesignate, null, null, "S10");
         //radarDesignation assumes 3
         tiosts.createTransition("S10", "modeTD = 3", Constants.GUARD_TRUE, changeModeRadar, null, null, "S11");
         tiosts.createTransition("S11", Constants.GUARD_TRUE, Constants.GUARD_TRUE, aircraftPosition, "rangeTD := r| azimuthTD := a| elevationTD := e", null, "S12");
         tiosts.createTransition("S12", "rangeTD = r AND azimuthTD = a AND elevationTD = e", Constants.GUARD_TRUE, targetPosition, null, null, "S13");
         tiosts.createTransition("S13", "targetTD = id", Constants.GUARD_TRUE, track, null, null, "S14");
         tiosts.createTransition("S14", "targetTD = id", clockGuard1, designate, null, null, "S18");
         //HUDDesignation assumes 2
         tiosts.createTransition("S10", "modeTD = 2", Constants.GUARD_TRUE, changeModeHUD, null, null, "S15");
         tiosts.createTransition("S15", Constants.GUARD_TRUE, Constants.GUARD_TRUE, reticlePositionHUDIn, "azimuthTD := a | elevationTD := e", null, "S16");
         tiosts.createTransition("S16", "targetTD = id", clockGuard1, designate, null, null, "S17");
         tiosts.createTransition("S17", "azimuthTD = a AND elevationTD = e", Constants.GUARD_TRUE, reticlePositionHUDOut, null, null, "S18");        
         tiosts.createTransition("S18", "modeTD = op", Constants.GUARD_TRUE, finishTargetDesignation, null, null, Constants.DEADLINE_EAGER, "S19");
         
         return tiosts;
		 
	 }

}
